/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */

/**
 * NuGat-API named Chameleon developed by Simon De Baets to Verimag.
 *
 */


package chameleon.model.NuGatManager;

import chameleon.model.NuGatStructure.compile.FlatHierarchy;
import chameleon.model.NuGatStructure.symbTable.SymbTable;
import chameleon.model.NuGatStructure.prop.PropDbGame;
import chameleon.model.NuGatStructure.opt.Opt;
import chameleon.model.NuGatStructure.utils.Node;
import chameleon.model.NuGatStructure.utils.Set;
import chameleon.model.NuGatStructure.utils.Expression;
import chameleon.model.NuGatStructure.fsm.SexpFsm;
import chameleon.model.NuGatStructure.fsm.FsmBuilder;
import chameleon.model.NuGatStructure.fsm.BddFsm;
import chameleon.model.NuGatStructure.fsm.GameSexpFsm;
import chameleon.model.NuGatStructure.bdd.Bdd;
import chameleon.model.NuGatStructure.bdd.ClusterList;
import chameleon.model.NuGatStructure.bdd.ClusterOptions;
import chameleon.model.NuGatStructure.bdd.BddTrans;
import chameleon.model.NuGatStructure.bdd.DdManager;
import chameleon.model.NuGatStructure.enc.BddEnc;
import chameleon.gameSolver.NuGat.NuGatInterface;
import chameleon.model.GameFactory;
import chameleon.model.NodeTrans;
import chameleon.model.automata.Automata;
import chameleon.model.automata.AutomataFactory;
import chameleon.model.formula.Formula;
import chameleon.model.formula.parser.BooleanParser;
import chameleon.model.formula.parser.LtlParser;
import chameleon.model.game.Game;
import chameleon.model.transitionFormat.AbstractTransition;
import chameleon.model.game.Tag;
import chameleon.model.game.transition.TransitionRelationDescription;
import chameleon.view.OutputManager;
import com.sun.jna.Pointer;
import com.sun.org.apache.xerces.internal.parsers.DOMParser;
import java.io.IOException;
import java.util.Hashtable;
import java.util.Iterator;
import java.util.Vector;
import java.util.logging.Level;
import java.util.logging.Logger;
import org.w3c.dom.Document;
import org.w3c.dom.Element;
import org.w3c.dom.NamedNodeMap;
import org.w3c.dom.NodeList;
import org.xml.sax.SAXException;

/**
 *
 * @author simon
 */


public class AddTransitionFactory {

   //key : graphical representation, Value : smv node_ptr
    private Hashtable smvMapTable_ = null;
    //key : id node, Value : string id node
    private Hashtable goalMapTable_;
    private Game game_;
    private NuGatInterface nugat_;
    private OutputManager outputManager_ = new OutputManager();


    public AddTransitionFactory (NuGatInterface nugat, Game game){
        nugat_ = nugat;
        game_ = game;
    }

    public NuGatInterface addTransition(int player, AbstractTransition transition) {

        SymbTableFactory factory = new SymbTableFactory(game_.getPropDatabase(),nugat_);
        smvMapTable_ = factory.createSymboleTable(null);
        
        if (transition.getTag()==Tag.SMVTRANS){
            addATransition(transition.getSmvTransition(), player);
        }
        else if (transition.getTag() == Tag.AUTOMATA || transition.getTag() == Tag.LTL){
            try {
                game_ = GameFactory.addTrans(game_, transition.getFile(), transition.getTag(), player);
            } catch (IOException ex) {
                Logger.getLogger(NuGatManager.class.getName()).log(Level.SEVERE, null, ex);
            }
            addTransitionsFromGoalFile(game_.getTransition(), transition.getTag(),player);
        }
        else
            throw new RuntimeException("AddTransitionFactory :: Unknow kind of transition");
        return nugat_;
    }
    /**
     * This function convert a string to a NuGaT transition. A NuGaT transition
     * is represented by a node_ptr. When the node_ptr is contructed, this function
     * call creationOfNewTransition that add new transition to the game.
     *
     *
     * @param transition
     * @param player
     */

    private void addATransition(String transition, int player) {
        try {
            Node node  = new Node(Pointer.NULL, nugat_);
            PropDbGame propDbGame = game_.getPropDatabase();
            
            Pointer scalar_fsm = propDbGame.getGameScalarSexpFsm();
            //First step : convert String to Formula
            BooleanParser parser = new BooleanParser(transition);
            Formula transFormula = parser.createFormula();

            //Second step : create the transition NuGat node

            Node transNode = transFormula.encFormula(nugat_, smvMapTable_);

            //Pointer transNode = encFormula(transFormula);

            Node findNode = findNode(player,transNode);


            FlatHierarchy flatHierarchy = new FlatHierarchy(game_.getGlobalSymbTable(),nugat_);
            Node transRelation = node.findNode(nugat_.AND,
                    flatHierarchy.getTrans().ptr(),
                    findNode.ptr());
            outputManager_.displayString("add transition : "+transRelation.sprintNode()+"\n");


            flatHierarchy.setTrans(transRelation);
            creationOFNewTransition(flatHierarchy, scalar_fsm, player);

        } catch (IOException ex) {
            Logger.getLogger(NuGatManager.class.getName()).log(Level.SEVERE, null, ex);
        }
    }

    /**
     * This function add the transition given in paramter (in flatHierarchy) to
     * the Game. To do this we use the function applySynchronousProduct
     * defined in NuSmv
     *
     *
     * @param flatHierarchy
     * @param scalar_fsm
     * @param player
     */

    private void creationOFNewTransition(FlatHierarchy flatHierarchy, Pointer scalar_fsm, int player) {
        //This code provide from NuSmv 2.5, of the file FsmBuilder.c (FsmBuilder_create_bdd_fsm_of_vars)
        ClusterList clusters;
        ClusterOptions clusterOptions;
        Set sortedVars;
        Node transExpr;
        Pointer iter;

        SexpFsm sexpFsm = getSexpFsm(player,scalar_fsm);
        FsmBuilder fsmBuilder = game_.getGlobalFsmBuilder();
        
        sortedVars = fsmBuilder.orderVarsList(game_.getBddEncoding(),
                                                  sexpFsm.getVarsList());


        //Here we substitute the transition relation by our new transition
        transExpr = flatHierarchy.getTrans();

        for (iter=sortedVars.getFirstIter(); !sortedVars.isEndIter(iter);
        iter=sortedVars.getNextIter(iter)) {
            Expression emptyExpr = new Expression(Pointer.NULL, nugat_); 
            
            Expression vtrans = sexpFsm.getVarTrans(sortedVars.getMember(iter));
            transExpr = new Node ((emptyExpr.andNil(new Expression (transExpr.ptr(),nugat_),
                    vtrans)).ptr(),
                  nugat_);
        }

        sortedVars.releaseSet(); /* no Pointerer needed */

        /* clusters construction */
        clusters = fsmBuilder.clusterizeExpr(
                game_.getBddEncoding(),
                transExpr.ptr());
        
        clusterOptions = new ClusterOptions(game_.getOptsHandlerInstance(), nugat_);

        SymbTable st = game_.getGlobalSymbTable();

        Bdd state_vars_cube = getStateVarsCube(player,st);


        BddEnc enc =  game_.getBddEncoding();

        Bdd next_state_vars_cube = enc.stateVarToNextStateVar(state_vars_cube);

        Opt opt = game_.getOptsHandlerInstance();

        DdManager bddBuilder = new DdManager(enc.getDdManager().ptr(),nugat_);
        
        BddTrans trans = new BddTrans(enc.getDdManager(),
                                clusters,
                                state_vars_cube,
                                bddBuilder.bddOne(),
                                next_state_vars_cube,
                                opt.getPartitionMethod(),
                                clusterOptions,
                                nugat_);



        clusters.destroy();
        clusterOptions.destroy(); /* this is no Pointerer needed */

        BddTrans transRelation = getTransitionRelation(player);

        transRelation.applySynchronousProduct(trans,
                state_vars_cube,
                bddBuilder.bddOne(),
                next_state_vars_cube);

    }

    private SexpFsm getSexpFsm(int player, Pointer scalar_fsm){
        GameSexpFsm gameSexpFsm = new GameSexpFsm(scalar_fsm, nugat_);
        if (player == 1)
            return gameSexpFsm.getPlayer1();
        else if (player == 2)
            return gameSexpFsm.getPlayer2();
        else
            throw new RuntimeException("NuGat Manager : GetGameSexpFsm : only two players game are suported");
    }

    /**
     * This funtion add to the game transitions described in a Goal File.
     *
     * @param transition
     * @param player
     */

    private void addTransitionsFromGoalFile(TransitionRelationDescription transition, int tag, int player) {
        //First step convert to NBW
        //transition.convert2NBW();
        
        //Second step parse the goal file
        Vector<NodeTrans> transitions = getTransitionRelation (transition.getFile().getPath(), tag);

        //Third step convert goal name to smv name
        Iterator iter = transitions.iterator();
        while(iter.hasNext()){
            addATransition(iter.next().toString(), player);
        }

    }

    private Node findNode(int player, Node trans) {
        Node node = new Node(Pointer.NULL,nugat_);
        if (player == 1)
            return node.findNode(nugat_.CONTEXT, nugat_.sym_intern(nugat_.PLAYER_NAME_1), trans.ptr());
        else
            return node.findNode(nugat_.CONTEXT, nugat_.sym_intern(nugat_.PLAYER_NAME_2), trans.ptr());
    }

    private Bdd getStateVarsCube(int player, SymbTable symbTable) {
        BddEnc bddEnc = game_.getBddEncoding();
        if (player == 1)
            return bddEnc.getLayerVarsCube(
                    symbTable.getLayer(nugat_.LAYER_PLAYER_1), 1);
        else if (player == 2)
            return bddEnc.getLayerVarsCube(
               symbTable.getLayer(nugat_.LAYER_PLAYER_2), 1);
        else
            throw new RuntimeException("AddTransition :: Only two players game are"
                    + "supported, here we have player : "+player);
    }

    private BddTrans getTransitionRelation(int player) {
        if (player == 1){
            BddFsm bddFsm = new BddFsm(game_.getBddFsmP1().ptr(),nugat_);
            return bddFsm.getTrans();
        }
        else if (player == 2){
            BddFsm bddFsm = new BddFsm(game_.getBddFsmP2().ptr(),nugat_);
            return bddFsm.getTrans();
        }
        else
            throw new RuntimeException("AddTransition :: Only two players game are"
                    + "supported, here we have player : "+player);
    }

    /**
     * This function return a transition relation given in a Goal File (automaton).
     *
     * @param path
     * @return
     */

    private Vector<NodeTrans> getTransitionRelation(String path, int tag) {
        Vector<NodeTrans> transitionRelation = new Vector<NodeTrans>();
        DOMParser parser = new DOMParser();
        try {
            parser.parse(path);
        } catch (SAXException ex) {
            Logger.getLogger(NuGatManager.class.getName()).log(Level.SEVERE, null, ex);
        } catch (IOException ex) {
            Logger.getLogger(NuGatManager.class.getName()).log(Level.SEVERE, null, ex);
        }
        Document document = parser.getDocument();

        Element automata = document.getDocumentElement();
        NodeList state = automata.getElementsByTagName("State");



        NodeList from = automata.getElementsByTagName("From");
        NodeList to = automata.getElementsByTagName("To");
        NodeList label = automata.getElementsByTagName("Label");

        //Creation of the goal map table
        goalMapTable_ = createGoalMapTable(state, label);
        
        int dec = 0;
        if (label.getLength() > from.getLength())
            dec = state.getLength();

        // COMPUTATION OF TRANSITION RELATION

        /**
         * If we have an automaton given by a user the translation is the following :
         *
         * input state & label -> next(state)
         *
         */

        if (tag == Tag.AUTOMATA){

            for (int i=0; i<from.getLength(); ++i){
                try {
                    String source = from.item(i).getFirstChild().getNodeValue();
                    String target = to.item(i).getFirstChild().getNodeValue();
                    String labelTrans = label.item(i+dec).getFirstChild().getNodeValue();
                    LtlParser ltlParser = new LtlParser();
                    ltlParser.createFormula((String) goalMapTable_.get(source));
                    ltlParser.createFormula((String) goalMapTable_.get(target));
                    ltlParser.createFormula(labelTrans);
                    NodeTrans trans = new NodeTrans(ltlParser.createFormula((String) goalMapTable_.get(source)),
                            ltlParser.createFormula((String) goalMapTable_.get(target)),
                            ltlParser.createFormula(labelTrans));
                    transitionRelation.add(trans.clone());
                } catch (IOException ex) {
                    Logger.getLogger(NuGatManager.class.getName()).log(Level.SEVERE, null, ex);
                }
            }
        }

        /**
         *  If we have an automaton that represents an LTL formula. It makes no
         * sense to use to state information because this state has no concrete
         * representation in NuGat. So we must use only the label on transition.
         *
         * The traduction is the following :
         *      for each node
         *          for each input edge
         *              transition is : input label -> (next(t) | next(t') | ... )
         *
         * where t is an output label.
         *
         */
        else if (tag == Tag.LTL){
            Automata transRelation = AutomataFactory.createAutomata(from, to, label, state, dec);
            transitionRelation = transRelation.getNuGatTransition();
        }

        return transitionRelation;
    }

    private Hashtable createGoalMapTable (NodeList state, NodeList label){
        Hashtable goalMapTable = new Hashtable();
        for (int i=0; i < state.getLength(); ++i){
            NamedNodeMap attributes = state.item(i).getAttributes();
            String key = attributes.getNamedItem("sid").getNodeValue();
            String[] value = label.item(i).getFirstChild().getNodeValue().split(",");
            goalMapTable.put(key, value[0]);
        }
        return goalMapTable;
    }


}
